/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package chameleon.model.satSolver;

import java.io.FileNotFoundException;
import java.io.IOException;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.reader.DimacsReader;
import org.sat4j.reader.ParseFormatException;
import org.sat4j.reader.Reader;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.ISolver;

/**
 * This class is wrapper for the satSolver sat4j.
 * @author simon
 */
public class SatSolver {

    private String problem_;

    public SatSolver(String problem){
        problem_ = problem;
    }

    /**
     * Return if a problem is satisfiable or not.
     *
     * @return
     * @throws FileNotFoundException
     * @throws ParseFormatException
     * @throws IOException
     * @throws org.sat4j.specs.TimeoutException
     * @throws ContradictionException
     */

    public boolean isSatisfiable() throws FileNotFoundException, ParseFormatException, IOException, org.sat4j.specs.TimeoutException, ContradictionException{
        ISolver solver = SolverFactory.newDefault();
        solver.setTimeout(3600); // 1 hour timeout
        Reader reader = new DimacsReader(solver);

        IProblem problem = reader.parseInstance(problem_);
        return problem.isSatisfiable();
    }

}
